import chalk from "chalk";

class Lit {
  constructor(ref, pol) {
    this.ref = ref;
    this.pol = pol;
    this.val = 0;
  }
  neg() { return new Lit(this.ref, -this.pol) }
  vah() { return this.ref.value * this.pol }
  // Mandatory for comparing with "=="
  valueOf() { return this.ref.index * this.pol}
}

const FriSat = function () {

  const {abs, sign} = Math;

  let clauses = [];

  let proTop = 0;
  let proMem = [];
  let decPos = [];

  let vars = []

  const assign = (lit, level, cause) => {
    Object.assign(lit.ref, {value: lit.pol, level, cause});
    for (let c of clauses) 
      for (let l of c) 
        if (l.ref.index === lit.ref.index)
          l.val = lit.pol * l.pol;
    proMem.push(lit);
  }

  const addClause = c => {
    c.length === 1 ? assign(c[0], 0, []) : clauses.push(c);
  }

  const parse = function (text) {
    let maxVar = 0;
    let lits = [];
    
    const makeVar = index => ({
      index,
      value: 0,
      epoch: 0,
    })

    const lines = text.split(/[\n\r]+/)
    for (let line of lines) {
      if (line.length === 0 && line === lines.at(-1)) continue;

      switch(line[0]) {
        case 'c': continue;
        case 'p':
          const [_, __, varsNumText, ___] = line.split(/[ \t]+/);
          maxVar = parseInt(varsNumText);
          vars = [...Array(maxVar + 1)]
            .map((_, i) => makeVar(i))
          break;
        default:
          let clauseLits = line
            .trim()
            .split(/[ \t]+/)
            .map(l => l.trim())
            .map(l => new Lit(vars[abs(l)], sign(l)));
          lits.push(...clauseLits);
      }
    }

    let clause = [];
    for (const lit of lits)
      if (lit != 0) clause.push(lit) 
      else addClause(clause.slice()), clause.splice(0); 

    console.log("PARSE FIN")
    clauses.origLen = clauses.length;
  } 

  const back = function (backDest) {

    if (decPos.length <= backDest) return;

    for (let i = proMem.length - 1; i >= decPos[backDest]; i--) {
      let p = proMem[i];
      p.ref.value = 0;
      for (let c of clauses) for (let l of c) if (l.ref.index === p.ref.index) l.val = 0;
    }

    proTop = decPos[backDest]
    proMem.splice(proTop)
    decPos.splice(backDest)
  }

  const fork = function () {
    let next = vars.find(v => v.value == 0);
    if (next) {
      decPos.push(proMem.length);
      assign(new Lit(next, 1), decPos.length, []);
    } else {
      return 1 
    }
  }

  let propElapse = 0;

  const prop = function() {
    // console.log("PROP")
    let start = performance.now();
    while (proTop < proMem.length) {              

      let p = proMem[proTop];                     
      proTop++;                                     

      for (let i = 0; i < clauses.length; i++) {
        const c = clauses[i];
        if (c[0] == -p) 
        [c[0], c[1]] = [c[1], c[0]];
      }

      nextCl: for (let c of clauses) if (c[0].val != 1 && c[1] == -p) {
       
        for (let rest = 2; rest < c.length; rest++) if (c[rest].val != -1) {                  
          [c[1], c[rest]] = [c[rest], c[1]];
          continue nextCl;                          
        }                                           

        if (c[0].val == -1) {                       
          propElapse += performance.now() - start;
          return c;                                   
        } else {                                      
          assign(c[0], p.ref.level, c);               
        }                                             
      }                                               
    }                                                 

    propElapse += performance.now() - start;
    return null;                                      

  }

  let epoch = 0;
  const test = function (cause) {
    epoch ++;

    let backDest;

    let hiestLevel = cause[0].ref.level;
    if (hiestLevel === 0) return {
      status: 'UNSAT',
    }
  
    let learnt = [];
    let routerCount = 0;
    let resLit = null;

    do {
      for (let l of cause.slice(resLit ? 1 :0)) 
        if (l.ref.epoch != epoch && l.ref.level > 0) {
          l.ref.epoch = epoch;
          l.ref.level >= hiestLevel ? routerCount++ : learnt.push(l);
        }
      
      do resLit = proMem.findLast(l => l.ref.epoch === epoch); 
        while(resLit.ref.level < hiestLevel);
      cause = resLit.ref.cause;
      resLit.ref.epoch = 0;
      routerCount--;
    } while (routerCount > 0);

    learnt.unshift(resLit.neg());
    
    if (learnt.length === 1) backDest = 0;
    else {
      let max = learnt[1];
      for (let l of learnt.slice(1)) if (l.ref.level > max.ref.level) max = l
      learnt.push(...learnt.splice(1, 1, max))
      backDest = learnt[1].ref.level;
    }

    return {
      learnt,
      backDest,
    };
  }

  const solve = function () {

    const start = performance.now()
    const FIELD_LEN = 20;

    let bumper = 0;
    console.log('c', "================ STATS ===============")
    console.log('c', chalk.bgYellowBright.redBright.bold("TOTAL(ms)".padStart(FIELD_LEN), 'PROP(ms)'.padStart(FIELD_LEN), "PROP RATIO".padStart(FIELD_LEN), "NOVO".padStart(FIELD_LEN), "NOVO RATIO".padStart(FIELD_LEN), "     "))
    console.log('c', 
      '0.000'.padStart(FIELD_LEN), 
      '0.000'.padStart(FIELD_LEN), 
      '0.00%'.padStart(FIELD_LEN), 
      "0".toString().padStart(FIELD_LEN), 
      '0.00%'.padStart(FIELD_LEN), 
      chalk.green.bold("START")
    )
    while (true) {
      const lap = performance.now() - start
      const orig = clauses.origLen;
      const novo = clauses.length - orig;
      const novoOverOrig = novo/orig;

      if (lap > (bumper + 1)*2000) {
        bumper ++;
        console.log('c', 
          lap.toFixed(3).padStart(FIELD_LEN), 
          propElapse.toFixed(3).padStart(FIELD_LEN), 
          chalk.bold(`${(propElapse * 100 / lap).toFixed(2)}%`.padStart(FIELD_LEN)), 
          novo.toString().padStart(FIELD_LEN),
          chalk.bold(`${novoOverOrig.toFixed(2)}%`.padStart(FIELD_LEN)),
        )
      }
      if ( lap > 120000) return { 
        s: 'UNKNOWN',
      };

      let conflict = prop();
      if (conflict) {
        let {status, learnt, backDest} = test(conflict);
        if (status) {
          console.log('c', 
            lap.toFixed(3).padStart(FIELD_LEN), 
            propElapse.toFixed(3).padStart(FIELD_LEN), 
            chalk.bold(`${(propElapse * 100 / lap).toFixed(2)}%`.padStart(FIELD_LEN)), 
            novo.toString().padStart(FIELD_LEN),
            chalk.bold(`${novoOverOrig.toFixed(2)}%`.padStart(FIELD_LEN)),
            chalk.red.bold("FINAL")
          )
          // console.log("c", lap.toFixed(3).padStart(FIELD_LEN), propElapse.toFixed(3).padStart(FIELD_LEN), chalk.bold(`${(propElapse * 100 / lap).toFixed(2)}%`.padStart(FIELD_LEN)), clauses.length.toString().padStart(FIELD_LEN), chalk.red.bold("FINAL"))
          console.log("c","======================================")
          return { 
            s: 'UNSAT', 
          };
        } 
       
        back(backDest);
        if (learnt.length == 1) {
          assign(learnt[0], 0, [])
        } else {
          addClause(learnt);
          assign(learnt[0], backDest, learnt);
        }
      } else if (fork()) {
        console.log('c', 
          lap.toFixed(3).padStart(FIELD_LEN), 
          propElapse.toFixed(3).padStart(FIELD_LEN), 
          chalk.bold(`${(propElapse * 100 / lap).toFixed(2)}%`.padStart(FIELD_LEN)), 
          novo.toString().padStart(FIELD_LEN),
          chalk.bold(`${novoOverOrig.toFixed(2)}%`.padStart(FIELD_LEN)),
          chalk.red.bold("FINAL")
        )

        // console.log('c', lap.toFixed(3).padStart(FIELD_LEN), propElapse.toFixed(3).padStart(FIELD_LEN), chalk.bold(`${(propElapse * 100 / lap).toFixed(2)}%`.padStart(FIELD_LEN)), clauses.length.toString().padStart(FIELD_LEN), chalk.red.bold("FINAL"))
        console.log('c',"======================================")
        return {
          s: 'SAT',
          v: vars.slice(1).map(v => `${v.value * v.index}`).join(' ') 
        };
      }
    }
  }

  return {
    parse,
    solve,
  }
};

export default FriSat;
